module MeteoCal
open util/boolean


//BASE TYPE SIGNATURES

sig Time {
	value: Int
}{
	value > 0
}

sig Name{}


//SIGNATURES

sig User {
	email: one Name,
	password: one Name,
	calendar: one Calendar,
	notifications: set Notification
}

sig Calendar {
	public: one Bool,
	owner: one User,
	events: set Event
}

sig Event {
	startTime: one Time,
	endTime: one Time,
	place: lone Name,
	public: one Bool,
	outdoor: one Bool,
	weatherForecast: lone WeatherForecast,
	disj usersWhoHaveDeclined, invitedUsers, participantUsers: set User,
	owner: one User
} {

//The start must come before the end
	startTime.value < endTime.value

//If it has no place, it has no forecast
	#place = 0 implies #weatherForecast = 0

//The owner cannot invite himself
	owner not in invitedUsers
	owner not in usersWhoHaveDeclined
	
//Every event is in at least one calendar
	some c : Calendar | this in c.events
}

sig WeatherForecast {
	isBad : one Bool
} {
//Every weather forecast is associated to an event
	some e : Event | this = e.weatherForecast
}

sig Notification {
	time : one Time,
	description : one Name,
	event : one Event
} {
//The notifications are received before the event starts
	time.value < event.startTime.value

//There is at least one owner who receives the notification
	some u : User | this in u.notifications
}

sig InvitationNotification extends Notification{}

sig BadWeatherNotification extends Notification{}


//FACTS

fact UserProperties {
//The email address is unique
	no disj u1, u2 : User | u1.email = u2.email

//To every user corresponds exactly one and only one calendar
	calendar = ~owner
}

fact BadWeatherNotificationProperties {
//Bad weather notifications are only for outdoor events with bad weather forecast
	all bwn : BadWeatherNotification | bwn.event.weatherForecast.isBad = True && bwn.event.outdoor = True
}

fact InvitationProperties {
//Every invited user receives one and only one notification per event
	all e : Event | all u : e.invitedUsers | one i : InvitationNotification | i in u.notifications &&  e = i.event

//Every invitation notification is received by one and only one user 
	all i : InvitationNotification | one u : User | i in u.notifications

//The number of invitation notifications is equal to the invited users
	#invitedUsers = #InvitationNotification
}


//ASSERTIONS
assert SameNumOfCalendarsAndUsers {
	#User = #Calendar
}
check SameNumOfCalendarsAndUsers

assert NoBadWeatherNotificationForIndoorOrSunnyEvents{
	all e : Event | e.outdoor = False || e.weatherForecast.isBad = False implies (no bwn : BadWeatherNotification | bwn.event = e)
}
check NoBadWeatherNotificationForIndoorOrSunnyEvents

assert NoSelfInvitations {
	no e : Event | e.owner in e.invitedUsers
}
check NoSelfInvitations


//PREDICATES

pred show() {}
run show for 3 but exactly 2 User

